(set-logic QF_UFLRA)
(set-info :source |
MathSat group

|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status sat)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun x4 () Real)
(declare-fun x5 () Real)
(declare-fun x6 () Real)
(declare-fun x7 () Real)
(declare-fun x8 () Real)
(declare-fun x9 () Real)
(declare-fun x10 () Real)
(declare-fun x11 () Real)
(declare-fun x12 () Real)
(declare-fun x13 () Real)
(declare-fun x14 () Real)
(declare-fun x15 () Real)
(declare-fun x16 () Real)
(declare-fun x17 () Real)
(declare-fun x18 () Real)
(declare-fun x19 () Real)
(declare-fun x20 () Real)
(declare-fun x21 () Real)
(declare-fun x22 () Real)
(declare-fun x23 () Real)
(declare-fun x24 () Real)
(declare-fun x25 () Real)
(declare-fun x26 () Real)
(declare-fun x27 () Real)
(declare-fun x28 () Real)
(declare-fun x29 () Real)
(declare-fun x30 () Real)
(declare-fun x31 () Real)
(declare-fun x32 () Real)
(declare-fun x33 () Real)
(declare-fun x34 () Real)
(declare-fun x35 () Real)
(declare-fun x36 () Real)
(declare-fun x37 () Real)
(declare-fun x38 () Real)
(declare-fun x39 () Real)
(declare-fun x40 () Real)
(declare-fun x41 () Real)
(declare-fun x42 () Real)
(declare-fun x43 () Real)
(declare-fun x44 () Real)
(declare-fun x45 () Real)
(declare-fun x46 () Real)
(declare-fun x47 () Real)
(declare-fun x48 () Real)
(declare-fun x49 () Real)
(declare-fun f0_1 (Real) Real)
(declare-fun f0_2 (Real Real) Real)
(declare-fun f0_3 (Real Real Real) Real)
(declare-fun f0_4 (Real Real Real Real) Real)
(declare-fun P0 () Bool)
(declare-fun P1 () Bool)
(declare-fun P2 () Bool)
(declare-fun P3 () Bool)
(declare-fun P4 () Bool)
(declare-fun P5 () Bool)
(declare-fun P6 () Bool)
(declare-fun P7 () Bool)
(declare-fun P8 () Bool)
(declare-fun P9 () Bool)
(declare-fun P10 () Bool)
(declare-fun P11 () Bool)
(declare-fun P12 () Bool)
(declare-fun P13 () Bool)
(declare-fun P14 () Bool)
(declare-fun P15 () Bool)
(declare-fun P16 () Bool)
(declare-fun P17 () Bool)
(declare-fun P18 () Bool)
(declare-fun P19 () Bool)
(declare-fun P20 () Bool)
(declare-fun P21 () Bool)
(declare-fun P22 () Bool)
(declare-fun P23 () Bool)
(declare-fun P24 () Bool)
(declare-fun P25 () Bool)
(declare-fun P26 () Bool)
(declare-fun P27 () Bool)
(declare-fun P28 () Bool)
(declare-fun P29 () Bool)
(declare-fun P30 () Bool)
(declare-fun P31 () Bool)
(declare-fun P32 () Bool)
(declare-fun P33 () Bool)
(declare-fun P34 () Bool)
(declare-fun P35 () Bool)
(declare-fun P36 () Bool)
(declare-fun P37 () Bool)
(declare-fun P38 () Bool)
(declare-fun P39 () Bool)
(declare-fun P40 () Bool)
(declare-fun P41 () Bool)
(declare-fun P42 () Bool)
(declare-fun P43 () Bool)
(declare-fun P44 () Bool)
(declare-fun P45 () Bool)
(declare-fun P46 () Bool)
(declare-fun P47 () Bool)
(declare-fun P48 () Bool)
(declare-fun P49 () Bool)
(assert (let ((?v_178 (<= (+ (- (* 3 x45) (* 15 x40)) (* 16 x34)) 7)) (?v_95 (* 19 x14)) (?v_231 (* 16 x9)) (?v_230 (* 8 x6)) (?v_32 (< (- (+ (* 13 x23) (* 24 x2)) (* 27 x39)) 6))) (let ((?v_33 (<= (+ (- (* 24 x14) ?v_230) (* 9 x17)) 9)) (?v_18 (< (- (- (* 24 x4) (* 9 x38)) (* 20 x43)) 10)) (?v_63 (* 9 x13))) (let ((?v_115 (< (+ (- (* 18 x31) ?v_63) (* 15 x13)) 4)) (?v_66 (* 24 x32)) (?v_146 (* 25 x12))) (let ((?v_208 (<= (- (+ (* 15 x48) (* 10 x20)) ?v_146) 15)) (?v_78 (< (- (+ (* 12 x43) (* 21 x28)) (* 3 x31)) 1)) (?v_192 (<= (- (+ (* 10 x9) (* 15 x9)) (* 12 x7)) 2)) (?v_128 (< (+ (- (* 6 x40) (* 13 x21)) (* 8 x44)) 22)) (?v_261 (<= (- (+ (* 2 x32) (* 9 x25)) (* 26 x30)) 15)) (?v_99 (f0_1 x4))) (let ((?v_202 (= ?v_99 x32)) (?v_17 (= (f0_2 x23 x43) (f0_1 x8))) (?v_16 (= x20 (f0_1 x19))) (?v_0 (f0_1 x37))) (let ((?v_9 (= x23 ?v_0)) (?v_19 (distinct (f0_1 x47) x7)) (?v_51 (distinct x23 (f0_2 x48 x49))) (?v_34 (= x0 (f0_2 x48 x5))) (?v_206 (distinct x40 x13)) (?v_234 (= (f0_2 x5 x46) (f0_2 x49 x40))) (?v_166 (= (f0_1 x1) (f0_2 x24 x27))) (?v_39 (f0_1 x21))) (let ((?v_61 (= x28 ?v_39)) (?v_139 (f0_1 x40))) (let ((?v_150 (distinct ?v_139 (f0_2 x49 x48))) (?v_103 (distinct ?v_139 x33)) (?v_31 (= x5 (f0_1 x36))) (?v_65 (f0_1 x12))) (let ((?v_29 (= ?v_65 (f0_2 x6 x0))) (?v_12 (= x29 (f0_1 x16))) (?v_254 (= x42 x49)) (?v_73 (= (f0_2 x40 x41) (f0_2 x1 x20))) (?v_94 (= ?v_65 (f0_2 x44 x5))) (?v_256 (= x26 (f0_2 x37 x14))) (?v_76 (distinct (f0_1 x26) x9)) (?v_114 (f0_1 x39))) (let ((?v_165 (distinct ?v_114 (f0_2 x15 x3))) (?v_56 (= (f0_2 x21 x43) (f0_1 x42))) (?v_140 (distinct (f0_1 x10) x16)) (?v_109 (f0_1 x33))) (let ((?v_182 (= (f0_2 x21 x29) ?v_109)) (?v_197 (= x46 x4)) (?v_22 (= (f0_2 x23 x21) x31)) (?v_119 (distinct (f0_1 x28) (f0_2 x8 x21))) (?v_167 (f0_1 x6))) (let ((?v_186 (= ?v_65 ?v_167)) (?v_43 (= ?v_39 (f0_2 x45 x13))) (?v_194 (= x13 (f0_2 x14 x21))) (?v_74 (distinct (f0_1 x18) (f0_2 x29 x33))) (?v_201 (f0_1 x29))) (let ((?v_221 (= (f0_1 x9) ?v_201)) (?v_106 (f0_1 x38))) (let ((?v_214 (distinct (f0_2 x35 x7) ?v_106)) (?v_26 (= (f0_2 x44 x23) x3)) (?v_224 (distinct (f0_1 x2) ?v_167)) (?v_28 (= (f0_2 x33 x34) ?v_99)) (?v_5 (= (f0_1 x32) x25)) (?v_27 (f0_1 x11))) (let ((?v_41 (distinct ?v_27 (f0_2 x47 x37))) (?v_15 (= (f0_2 x0 x5) x13)) (?v_67 (= ?v_109 (f0_2 x42 x9))) (?v_216 (= ?v_201 (f0_1 x45))) (?v_88 (= (f0_2 x17 x47) x9)) (?v_59 (= (f0_2 x47 x18) (f0_1 x20))) (?v_23 (= (f0_2 x49 x41) ?v_106)) (?v_58 (distinct (f0_1 x17) x25)) (?v_162 (= ?v_0 x17)) (?v_57 (distinct ?v_27 ?v_114)) (?v_160 (distinct (f0_2 x37 x11) ?v_65)) (?v_53 (distinct (f0_2 x45 x15) x30)) (?v_49 (not ?v_9)) (?v_179 (not ?v_206))) (let ((?v_89 (not ?v_59)) (?v_251 (not ?v_18)) (?v_113 (not ?v_22)) (?v_82 (not P14)) (?v_4 (not P42)) (?v_176 (not ?v_162)) (?v_158 (not P9)) (?v_255 (not ?v_34)) (?v_20 (not P46)) (?v_44 (not ?v_19)) (?v_218 (not ?v_32)) (?v_69 (not ?v_26)) (?v_102 (not ?v_254)) (?v_48 (not ?v_17)) (?v_135 (not ?v_56)) (?v_92 (not ?v_197)) (?v_8 (not P17)) (?v_24 (not P8)) (?v_10 (not P41)) (?v_11 (not ?v_234)) (?v_35 (not P28)) (?v_80 (not P37)) (?v_97 (not P6)) (?v_108 (not ?v_12)) (?v_127 (not P44)) (?v_38 (not ?v_256)) (?v_96 (not P2)) (?v_86 (not P3)) (?v_121 (not P15)) (?v_177 (not ?v_74)) (?v_170 (not ?v_33)) (?v_68 (not ?v_31)) (?v_110 (not P22)) (?v_25 (not ?v_23)) (?v_105 (not P36)) (?v_42 (not ?v_28)) (?v_79 (not ?v_43)) (?v_152 (not ?v_53)) (?v_237 (not P29)) (?v_196 (not ?v_41)) (?v_245 (not P0)) (?v_153 (not P21)) (?v_149 (not ?v_29)) (?v_84 (not P38)) (?v_131 (not P47)) (?v_133 (not ?v_221)) (?v_120 (not ?v_51)) (?v_132 (not P33)) (?v_172 (not P16)) (?v_239 (not ?v_57)) (?v_64 (not ?v_58)) (?v_129 (not P34)) (?v_207 (not ?v_115)) (?v_81 (not ?v_67)) (?v_164 (not ?v_73)) (?v_249 (not P11)) (?v_212 (not ?v_61)) (?v_183 (not ?v_76)) (?v_122 (not P4)) (?v_107 (not P1)) (?v_226 (not P31)) (?v_161 (not ?v_78)) (?v_184 (not P32)) (?v_191 (not P13)) (?v_116 (not P35)) (?v_217 (not ?v_16)) (?v_174 (not P40)) (?v_134 (not ?v_88)) (?v_204 (not P25)) (?v_173 (not ?v_94)) (?v_117 (not ?v_192)) (?v_243 (not ?v_202)) (?v_175 (not P24)) (?v_136 (not ?v_214)) (?v_141 (not ?v_178)) (?v_222 (not P23)) (?v_193 (not P19)) (?v_223 (not ?v_119)) (?v_219 (not P26)) (?v_246 (not P7)) (?v_138 (not ?v_261)) (?v_156 (not ?v_208)) (?v_253 (not P43)) (?v_257 (not ?v_5)) (?v_188 (not ?v_160)) (?v_171 (not P49)) (?v_209 (not P10)) (?v_242 (not ?v_128)) (?v_180 (not ?v_15)) (?v_240 (not ?v_182)) (?v_203 (not P20)) (?v_213 (not ?v_140)) (?v_199 (not P5)) (?v_264 (not P12)) (?v_259 (not P27)) (?v_229 (not P39)) (?v_244 (not P48)) (?v_235 (not ?v_103)) (?v_220 (not ?v_165)) (?v_247 (not P45)) (?v_252 (not ?v_224)) (?v_233 (not ?v_150)) (?v_258 (not P18)) (?v_248 (not ?v_186)) (?v_250 (not P30)) (?v_262 (not ?v_216)) (?v_260 (not ?v_194)) (?v_2 (< (+ (* 24 x26) (* 8 x26) (* 4 x44)) 14)) (?v_7 (< (+ (* 20 x9) ?v_63 (* 20 x16)) 22))) (let ((?v_14 (not ?v_7)) (?v_187 (< (- (+ x18 (* 21 x40)) (* 14 x13)) 24))) (let ((?v_50 (not ?v_187)) (?v_85 (<= (- (+ ?v_95 (* 13 x1)) 0) 4)) (?v_45 (not ?v_2)) (?v_75 (distinct (* 14 x25) 4)) (?v_52 (<= (+ (- (* 20 x46) x44) (* 11 x12)) 9)) (?v_55 (= (+ (- 0 (* 15 x21)) (* 3 x28)) 29))) (let ((?v_263 (not ?v_55)) (?v_54 (<= (+ (- 0 (* 9 x42)) (* 18 x29)) 11))) (let ((?v_83 (not ?v_54)) (?v_124 (<= (+ ?v_66 (* 2 x14) (* 8 x19)) 18))) (let ((?v_265 (not ?v_124)) (?v_227 (< (- (- 0 (* 8 x7)) (* 27 x43)) 25))) (let ((?v_198 (not ?v_227)) (?v_123 (not ?v_52)) (?v_155 (not ?v_85)) (?v_232 (not ?v_75)) (?v_1 (<= (- (- 0 (* 4 x29)) 0) (- 21))) (?v_40 (< (- (+ (* 19 x8) (* 24 x5)) 0) (- 21)))) (let ((?v_13 (not ?v_1)) (?v_3 (= (- (+ (* 21 x24) x35) (* 15 x36)) (- 20))) (?v_6 (<= (+ (- (* (- 10) x12) (* 21 x27)) (* 19 x22)) (- 28))) (?v_71 (<= (- (+ (* 15 x32) (* 18 x39)) (* 25 x17)) (- 21))) (?v_104 (< (- (* (- 21) x14) (* 25 x33)) 23))) (let ((?v_195 (not ?v_104)) (?v_60 (< (- (- (* (- 1) x31) (* 21 x36)) (* 5 x4)) 14)) (?v_77 (<= (- (+ (* (- 7) x15) (* 9 x26)) (* 4 x14)) (- 11)))) (let ((?v_126 (not ?v_77)) (?v_87 (<= (+ (* 2 x3) (* 2 x19) (* 13 x35)) (- 22)))) (let ((?v_181 (not ?v_87)) (?v_62 (distinct (+ (* (- 14) x1) (* 12 x36) (* 4 x4)) (- 19)))) (let ((?v_37 (not ?v_62)) (?v_46 (= (- (- (* (- 14) x6) (* 8 x40)) (* 17 x14)) 17)) (?v_148 (<= (+ (* 2 x45) (* 5 x47) (* 23 x13)) (- 14)))) (let ((?v_21 (not ?v_148)) (?v_211 (not ?v_3)) (?v_228 (or ?v_1 ?v_110)) (?v_30 (<= (- (+ (* (- 25) x29) (* 27 x5)) (* 17 x37)) (- 24)))) (let ((?v_168 (not ?v_30)) (?v_70 (= (- (+ (* (- 5) x19) (* 11 x42)) (* 5 x22)) 6)) (?v_90 (distinct (+ (* 23 x3) (* 13 x49) (* 16 x38)) (- 21)))) (let ((?v_36 (not ?v_90)) (?v_111 (<= (+ (* (- 7) x19) ?v_231 (* 13 x45)) 24))) (let ((?v_142 (not ?v_111)) (?v_112 (<= (- (- (* (- 24) x9) (* 25 x13)) (* 21 x42)) (- 15))) (?v_125 (<= (+ (* (- 7) x38) (* 15 x3) (* 13 x39)) 28)) (?v_210 (not ?v_40)) (?v_47 (< (- (+ (* (- 22) x31) ?v_66) (* 22 x33)) (- 22)))) (let ((?v_238 (not ?v_47)) (?v_144 (<= (- (- (* 10 x37) (* 17 x5)) (* 19 x9)) (- 12)))) (let ((?v_100 (not ?v_144)) (?v_130 (distinct (+ (- (* (- 11) x41) (* 6 x18)) (* 10 x47)) 27))) (let ((?v_91 (not ?v_130)) (?v_72 (<= (- (+ ?v_146 (* 10 x24)) (* 23 x34)) (- 29))) (?v_98 (not ?v_70)) (?v_93 (not ?v_71)) (?v_159 (<= (- (- (* (- 2) x37) (* 5 x6)) (* 11 x36)) 25)) (?v_154 (<= (+ (* 2 x6) (* 27 x34) (* 11 x11)) (- 24)))) (let ((?v_169 (not ?v_154)) (?v_200 (<= (+ (* (- 25) x5) (* 27 x17) (* 7 x9)) 15))) (let ((?v_190 (not ?v_200)) (?v_101 (< (+ (* 10 x18) (* 4 x6) (* 5 x2)) (- 8))) (?v_163 (<= (- (+ (* (- 26) x5) ?v_95) (* 14 x46)) 5))) (let ((?v_205 (not ?v_163)) (?v_145 (<= (- (- (* (- 15) x12) (* 8 x23)) (* 5 x16)) 0)) (?v_137 (not ?v_101)) (?v_147 (not ?v_112)) (?v_143 (not ?v_72)) (?v_118 (<= (- (+ (* (- 18) x30) (* 6 x2)) (* 12 x11)) 3)) (?v_151 (not ?v_46)) (?v_157 (not ?v_125))) (let ((?v_215 (not ?v_118)) (?v_185 (not ?v_60)) (?v_189 (not ?v_6)) (?v_225 (not ?v_145)) (?v_241 (not ?v_159)) (?v_236 (<= (- (- (* (- 9) x10) ?v_230) ?v_231) 13))) (let ((?v_266 (not ?v_236))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or ?v_49 ?v_179) ?v_89) (or (or ?v_251 P25) ?v_113)) (or (or ?v_1 ?v_40) ?v_82)) (or (or ?v_15 ?v_41) P11)) (or (or ?v_2 ?v_14) ?v_4)) (or (or ?v_176 P17) ?v_158)) (or (or ?v_13 P49) ?v_255)) (or (or ?v_2 ?v_20) ?v_3)) (or (or ?v_44 ?v_3) ?v_6)) (or (or ?v_71 ?v_218) ?v_69)) (or (or ?v_102 ?v_48) ?v_135)) (or (or ?v_92 ?v_8) ?v_4)) (or (or ?v_195 ?v_5) ?v_24)) (or (or ?v_10 P15) ?v_5)) (or (or ?v_6 ?v_60) ?v_7)) (or (or ?v_11 ?v_35) P15)) (or (or ?v_8 P5) ?v_9)) (or (or P40 P37) ?v_50)) (or (or ?v_128 ?v_85) P29)) (or (or ?v_80 ?v_97) P25)) (or (or ?v_108 ?v_126) ?v_127)) (or (or ?v_38 P36) ?v_96)) (or (or ?v_10 ?v_86) ?v_11)) (or (or ?v_12 P32) ?v_13)) (or (or ?v_121 ?v_78) ?v_29)) (or (or P47 ?v_14) P25)) (or (or ?v_15 P9) ?v_181)) (or (or ?v_177 ?v_16) ?v_37)) (or (or P22 ?v_16) ?v_170)) (or (or ?v_68 ?v_17) P15)) (or (or ?v_10 ?v_46) ?v_18)) (or (or ?v_19 ?v_21) ?v_211)) (or ?v_228 P7)) (or (or ?v_168 P36) ?v_20)) (or (or ?v_21 ?v_67) ?v_70)) (or (or ?v_22 ?v_28) ?v_36)) (or (or ?v_45 P35) ?v_25)) (or (or ?v_75 ?v_142) ?v_23)) (or (or ?v_14 ?v_1) ?v_52)) (or (or ?v_105 ?v_2) P15)) (or (or ?v_112 ?v_24) ?v_25)) (or (or ?v_24 ?v_125) ?v_26)) (or (or ?v_57 ?v_42) ?v_29)) (or (or ?v_30 ?v_4) ?v_31)) (or (or ?v_79 ?v_152) ?v_32)) (or (or ?v_33 ?v_34) P22)) (or (or ?v_35 ?v_51) ?v_36)) (or (or ?v_37 ?v_103) ?v_263)) (or (or ?v_17 ?v_38) ?v_61)) (or (or ?v_210 P15) ?v_237)) (or (or P10 ?v_196) ?v_13)) (or (or ?v_245 ?v_42) ?v_34)) (or (or ?v_153 ?v_43) ?v_54)) (or (or P31 P37) ?v_44)) (or (or ?v_34 ?v_45) ?v_58)) (or (or ?v_149 ?v_6) ?v_47)) (or (or ?v_46 ?v_84) ?v_238)) (or (or ?v_131 ?v_48) ?v_49)) (or (or ?v_50 ?v_133) ?v_120)) (or (or ?v_132 P33) ?v_52)) (or (or ?v_172 ?v_100) ?v_43)) (or (or ?v_53 ?v_140) P11)) (or (or ?v_45 ?v_91) P17)) (or (or ?v_9 ?v_11) ?v_83)) (or (or ?v_55 ?v_56) ?v_239)) (or (or ?v_64 ?v_129) ?v_59)) (or (or ?v_60 P46) ?v_61)) (or (or P15 ?v_62) ?v_72)) (or (or ?v_207 ?v_61) ?v_64)) (or (or P7 ?v_41) ?v_94)) (or (or ?v_265 ?v_81) ?v_60)) (or (or ?v_68 ?v_164) P43)) (or (or P17 ?v_198) ?v_69)) (or (or ?v_98 P4) P7)) (or (or P37 ?v_4) ?v_93)) (or (or ?v_72 ?v_249) ?v_76)) (or (or P27 P2) ?v_159)) (or (or ?v_73 ?v_212) ?v_88)) (or (or P37 ?v_10) ?v_169)) (or (or ?v_74 P43) ?v_73)) (or (or ?v_75 ?v_7) ?v_183)) (or (or ?v_1 ?v_122) P46)) (or (or P47 ?v_107) ?v_226)) (or (or ?v_77 ?v_31) ?v_161)) (or (or P15 ?v_184) ?v_79)) (or (or ?v_7 ?v_191) P11)) (or (or ?v_80 ?v_190) ?v_81)) (or (or ?v_82 ?v_83) ?v_21)) (or (or ?v_84 ?v_116) ?v_217)) (or (or ?v_101 P24) ?v_85)) (or (or ?v_74 ?v_174) ?v_86)) (or (or ?v_87 P45) ?v_134)) (or (or ?v_89 ?v_90) ?v_77)) (or (or ?v_36 ?v_91) ?v_92)) (or (or P23 P23) ?v_93)) (or (or ?v_92 P24) ?v_204)) (or (or ?v_173 ?v_205) ?v_123)) (or (or ?v_20 P23) ?v_48)) (or (or ?v_117 ?v_91) ?v_82)) (or (or ?v_24 ?v_73) P30)) (or (or P12 ?v_96) ?v_97)) (or (or ?v_37 ?v_98) ?v_155)) (or (or P31 ?v_243) ?v_100)) (or (or ?v_101 ?v_28) ?v_102)) (or (or ?v_145 ?v_103) ?v_104)) (or (or ?v_175 ?v_34) P4)) (or (or ?v_105 P38) ?v_136)) (or (or ?v_107 ?v_92) ?v_32)) (or (or ?v_108 ?v_182) ?v_107)) (or (or ?v_110 ?v_45) P49)) (or (or ?v_137 ?v_81) ?v_111)) (or (or ?v_147 P13) ?v_113)) (or (or ?v_3 ?v_76) ?v_141)) (or (or ?v_165 ?v_222) ?v_83)) (or (or ?v_1 ?v_143) ?v_115)) (or (or ?v_118 ?v_83) ?v_80)) (or (or ?v_69 ?v_119) ?v_193)) (or (or ?v_116 ?v_117) P37)) (or (or P38 ?v_118) ?v_223)) (or (or ?v_120 ?v_219) ?v_4)) (or (or ?v_74 ?v_121) P11)) (or (or ?v_110 ?v_122) ?v_151)) (or (or ?v_123 ?v_10) P10)) (or (or ?v_23 ?v_124) ?v_71)) (or (or ?v_85 ?v_8) ?v_37)) (or (or ?v_157 P17) P28)) (or (or P10 ?v_246) ?v_92)) (or (or ?v_100 ?v_126) ?v_80)) (or (or ?v_113 ?v_58) ?v_127)) (or (or P10 P12) ?v_128)) (or (or ?v_129 ?v_130) ?v_131)) (or (or ?v_24 P40) ?v_129)) (or (or ?v_91 ?v_138) ?v_224)) (or (or ?v_132 ?v_120) ?v_82)) (or (or ?v_28 ?v_90) ?v_43)) (or (or ?v_2 ?v_127) ?v_133)) (or (or ?v_49 P41) ?v_68)) (or (or ?v_120 ?v_120) ?v_134)) (or (or ?v_16 ?v_25) ?v_67)) (or (or ?v_48 ?v_135) ?v_136)) (or (or ?v_57 ?v_137) ?v_112)) (or (or ?v_88 ?v_17) ?v_122)) (or (or ?v_138 ?v_232) ?v_119)) (or (or ?v_150 ?v_140) P48)) (or (or ?v_141 ?v_102) ?v_142)) (or (or ?v_31 ?v_75) ?v_143)) (or (or ?v_135 ?v_105) ?v_9)) (or (or ?v_62 ?v_43) ?v_144)) (or (or ?v_41 ?v_145) ?v_141)) (or (or ?v_156 P10) ?v_132)) (or (or ?v_6 P11) ?v_78)) (or (or ?v_85 ?v_90) ?v_147)) (or (or ?v_253 ?v_148) ?v_257)) (or (or ?v_45 ?v_47) P4)) (or (or ?v_149 ?v_45) ?v_135)) (or (or ?v_14 ?v_111) ?v_150)) (or (or ?v_115 ?v_84) ?v_151)) (or (or ?v_215 P4) P42)) (or (or P39 ?v_30) P41)) (or (or ?v_124 P8) P21)) (or (or ?v_84 ?v_37) P20)) (or (or ?v_152 ?v_81) ?v_118)) (or (or ?v_127 ?v_85) ?v_153)) (or (or ?v_56 ?v_115) ?v_154)) (or (or ?v_2 ?v_104) ?v_188)) (or (or ?v_155 ?v_171) ?v_25)) (or (or ?v_151 P34) ?v_148)) (or (or ?v_127 ?v_53) ?v_7)) (or (or ?v_17 ?v_29) ?v_156)) (or (or P13 ?v_97) ?v_154)) (or (or ?v_157 ?v_209) ?v_15)) (or (or P44 ?v_121) ?v_8)) (or (or ?v_242 ?v_158) ?v_10)) (or (or ?v_159 (not ?v_166)) ?v_185)) (or (or ?v_160 P47) ?v_17)) (or (or ?v_23 ?v_135) P49)) (or (or ?v_18 ?v_161) ?v_115)) (or (or ?v_162 ?v_76) ?v_163)) (or (or P30 ?v_164) ?v_131)) (or (or ?v_157 ?v_160) ?v_35)) (or (or ?v_77 ?v_164) ?v_165)) (or (or ?v_18 P6) ?v_103)) (or (or ?v_75 P14) P16)) (or (or ?v_29 ?v_25) ?v_166)) (or (or ?v_141 P36) ?v_186)) (or (or P30 P38) ?v_52)) (or (or P15 ?v_55) ?v_165)) (or (or P10 ?v_141) ?v_49)) (or (or ?v_125 ?v_62) ?v_50)) (or (or ?v_150 ?v_168) ?v_78)) (or (or ?v_169 ?v_104) ?v_38)) (or (or ?v_170 ?v_112) ?v_80)) (or (or ?v_131 ?v_171) ?v_42)) (or (or ?v_172 ?v_151) ?v_72)) (or (or P43 ?v_173) ?v_117)) (or (or P45 ?v_136) ?v_98)) (or (or ?v_22 ?v_174) ?v_119)) (or (or ?v_175 P20) P33)) (or (or P5 ?v_165) P47)) (or (or ?v_125 ?v_176) ?v_78)) (or (or ?v_41 ?v_24) ?v_119)) (or (or ?v_147 ?v_180) ?v_177)) (or (or ?v_138 ?v_119) P7)) (or (or ?v_178 ?v_77) ?v_165)) (or (or ?v_96 ?v_179) ?v_10)) (or (or ?v_20 ?v_180) P8)) (or (or P20 ?v_157) P25)) (or (or ?v_92 P6) ?v_19)) (or (or ?v_32 P19) ?v_181)) (or (or ?v_240 ?v_46) ?v_194)) (or (or ?v_183 ?v_67) ?v_164)) (or (or ?v_36 ?v_189) ?v_9)) (or (or ?v_184 ?v_165) ?v_92)) (or (or ?v_152 ?v_35) ?v_23)) (or (or ?v_19 P9) ?v_161)) (or (or ?v_64 ?v_127) ?v_185)) (or (or ?v_83 ?v_126) ?v_128)) (or (or ?v_48 ?v_78) ?v_203)) (or (or ?v_56 ?v_186) ?v_187)) (or (or P17 ?v_188) ?v_189)) (or (or P38 ?v_49) ?v_16)) (or (or ?v_1 ?v_190) ?v_191)) (or (or ?v_163 ?v_192) ?v_149)) (or (or ?v_145 ?v_193) ?v_140)) (or (or ?v_75 ?v_113) ?v_171)) (or (or P0 ?v_79) P21)) (or (or ?v_194 ?v_165) ?v_195)) (or (or ?v_196 ?v_177) ?v_213)) (or (or P48 ?v_41) ?v_101)) (or (or ?v_199 ?v_264) P14)) (or (or ?v_76 ?v_52) ?v_100)) (or (or P26 ?v_104) ?v_137)) (or (or ?v_17 ?v_197) ?v_198)) (or (or ?v_45 ?v_198) ?v_105)) (or (or ?v_124 ?v_121) ?v_197)) (or (or P30 ?v_73) ?v_61)) (or (or ?v_199 ?v_182) ?v_179)) (or (or P29 ?v_67) ?v_200)) (or (or ?v_52 ?v_52) ?v_32)) (or (or P13 ?v_11) ?v_216)) (or (or ?v_202 P12) ?v_118)) (or (or ?v_107 ?v_203) ?v_259)) (or (or ?v_225 ?v_18) ?v_204)) (or (or ?v_98 ?v_229) ?v_80)) (or (or ?v_165 ?v_81) ?v_178)) (or (or ?v_244 P47) P40)) (or (or ?v_12 P5) ?v_205)) (or (or P31 ?v_198) ?v_71)) (or (or ?v_61 ?v_203) ?v_115)) (or (or ?v_196 P23) ?v_206)) (or (or ?v_119 ?v_138) ?v_204)) (or (or ?v_207 ?v_208) ?v_185)) (or (or ?v_123 ?v_57) ?v_145)) (or (or ?v_164 ?v_4) ?v_209)) (or (or ?v_159 ?v_241) ?v_210)) (or (or ?v_161 ?v_207) P35)) (or (or ?v_189 ?v_235) ?v_129)) (or (or ?v_153 P45) ?v_1)) (or (or ?v_211 ?v_212) ?v_149)) (or (or ?v_213 ?v_100) ?v_202)) (or (or ?v_214 P2) ?v_46)) (or (or ?v_215 ?v_93) ?v_216)) (or (or ?v_102 ?v_23) ?v_217)) (or (or ?v_184 ?v_28) ?v_218)) (or (or ?v_145 ?v_16) ?v_220)) (or (or ?v_73 ?v_219) ?v_32)) (or (or ?v_88 ?v_26) ?v_220)) (or (or ?v_118 ?v_205) ?v_145)) (or (or P46 ?v_161) P30)) (or (or ?v_212 ?v_221) P30)) (or (or ?v_222 ?v_30) ?v_107)) (or (or P2 P10) ?v_37)) (or (or ?v_8 P3) ?v_223)) (or (or ?v_177 ?v_74) ?v_34)) (or (or ?v_17 ?v_56) ?v_88)) (or (or ?v_26 P16) ?v_247)) (or (or ?v_104 P1) ?v_70)) (or (or ?v_3 P25) ?v_252)) (or (or ?v_151 ?v_165) ?v_77)) (or (or ?v_57 ?v_23) ?v_174)) (or (or ?v_225 ?v_215) ?v_226)) (or (or P37 ?v_100) ?v_227)) (or ?v_228 ?v_161)) (or (or P15 ?v_108) P8)) (or (or P42 ?v_198) ?v_2)) (or (or ?v_229 ?v_219) ?v_110)) (or (or ?v_198 ?v_172) ?v_58)) (or (or P14 ?v_147) ?v_87)) (or (or ?v_41 ?v_236) ?v_227)) (or (or ?v_157 ?v_14) P39)) (or (or P20 P43) ?v_69)) (or (or ?v_233 ?v_170) ?v_232)) (or (or ?v_2 ?v_120) ?v_80)) (or (or P24 ?v_164) ?v_205)) (or (or ?v_233 ?v_52) P8)) (or (or ?v_217 ?v_2) ?v_54)) (or (or P44 ?v_127) ?v_186)) (or (or ?v_234 ?v_158) ?v_43)) (or (or ?v_235 ?v_234) ?v_192)) (or (or ?v_83 P28) ?v_101)) (or (or P21 ?v_150) ?v_12)) (or (or ?v_119 ?v_190) ?v_22)) (or (or ?v_155 ?v_58) ?v_161)) (or (or ?v_76 P14) ?v_154)) (or (or ?v_57 ?v_81) ?v_113)) (or (or ?v_157 ?v_52) ?v_223)) (or (or ?v_75 ?v_21) P44)) (or (or ?v_33 P48) ?v_34)) (or (or P25 ?v_182) ?v_142)) (or (or ?v_111 ?v_19) P38)) (or (or P43 ?v_85) ?v_165)) (or (or P45 ?v_24) ?v_137)) (or (or ?v_52 ?v_117) ?v_98)) (or (or P46 ?v_147) ?v_104)) (or (or ?v_15 ?v_177) ?v_98)) (or (or P23 ?v_141) P18)) (or (or ?v_36 ?v_90) ?v_107)) (or (or ?v_121 ?v_52) P32)) (or (or P21 ?v_83) ?v_22)) (or (or ?v_198 ?v_44) ?v_187)) (or (or ?v_136 ?v_258) ?v_8)) (or (or ?v_236 ?v_237) P18)) (or (or P3 ?v_238) ?v_2)) (or (or ?v_185 ?v_162) P4)) (or (or P48 ?v_148) ?v_100)) (or (or ?v_53 P43) ?v_221)) (or (or ?v_154 P44) ?v_239)) (or (or P19 ?v_73) ?v_208)) (or (or P46 ?v_108) ?v_6)) (or (or ?v_151 ?v_248) ?v_41)) (or (or ?v_142 P22) ?v_102)) (or (or P11 ?v_127) ?v_250)) (or (or ?v_240 ?v_165) ?v_78)) (or (or ?v_117 P11) P20)) (or (or P37 ?v_176) ?v_7)) (or (or ?v_157 ?v_54) ?v_151)) (or (or P21 ?v_141) ?v_85)) (or (or P15 ?v_240) ?v_177)) (or (or ?v_152 ?v_195) ?v_184)) (or (or ?v_162 ?v_145) ?v_29)) (or (or ?v_205 ?v_208) P10)) (or (or ?v_241 ?v_115) ?v_188)) (or (or ?v_101 ?v_262) ?v_57)) (or (or ?v_162 ?v_75) ?v_131)) (or (or P8 ?v_126) ?v_242)) (or (or ?v_76 ?v_240) ?v_195)) (or (or ?v_155 ?v_243) ?v_103)) (or (or ?v_108 ?v_229) ?v_11)) (or (or ?v_1 ?v_44) ?v_155)) (or (or P0 ?v_149) ?v_244)) (or (or P39 ?v_244) ?v_245)) (or (or ?v_110 ?v_137) ?v_127)) (or (or ?v_77 ?v_180) ?v_206)) (or (or ?v_4 ?v_10) ?v_197)) (or (or P9 ?v_48) ?v_91)) (or (or ?v_69 ?v_134) ?v_243)) (or (or ?v_21 ?v_43) ?v_246)) (or (or ?v_237 ?v_136) ?v_153)) (or (or ?v_260 ?v_44) P34)) (or (or ?v_137 ?v_144) P43)) (or (or ?v_247 ?v_155) ?v_87)) (or (or ?v_151 ?v_73) ?v_150)) (or (or ?v_138 ?v_182) ?v_226)) (or (or ?v_23 ?v_193) P17)) (or (or ?v_13 ?v_41) ?v_206)) (or (or ?v_38 ?v_179) ?v_10)) (or (or ?v_78 ?v_181) ?v_25)) (or (or ?v_169 ?v_55) ?v_28)) (or (or ?v_89 ?v_186) ?v_54)) (or (or ?v_248 ?v_68) ?v_188)) (or (or ?v_216 ?v_244) ?v_34)) (or (or ?v_100 ?v_93) ?v_232)) (or (or P39 ?v_71) ?v_245)) (or (or ?v_98 ?v_249) P30)) (or (or ?v_153 ?v_172) ?v_119)) (or (or ?v_193 ?v_233) P18)) (or (or ?v_156 ?v_151) ?v_49)) (or (or ?v_250 P31) P22)) (or (or ?v_15 ?v_8) ?v_186)) (or (or ?v_181 ?v_22) ?v_237)) (or (or ?v_190 P34) ?v_165)) (or (or ?v_194 ?v_53) ?v_251)) (or (or ?v_239 ?v_179) ?v_113)) (or (or ?v_243 ?v_194) ?v_129)) (or (or ?v_252 ?v_83) ?v_144)) (or (or ?v_57 ?v_53) ?v_48)) (or (or ?v_87 ?v_5) ?v_179)) (or (or ?v_7 ?v_4) ?v_34)) (or (or ?v_140 ?v_91) ?v_180)) (or (or ?v_154 P25) ?v_84)) (or (or ?v_24 ?v_133) ?v_81)) (or (or ?v_111 ?v_158) ?v_253)) (or (or ?v_29 ?v_17) ?v_122)) (or (or ?v_150 ?v_226) ?v_19)) (or (or P18 ?v_210) ?v_254)) (or (or P33 ?v_185) ?v_36)) (or (or ?v_96 P49) P27)) (or (or ?v_92 ?v_169) ?v_163)) (or (or ?v_254 ?v_234) ?v_206)) (or (or ?v_86 ?v_222) ?v_5)) (or (or ?v_177 ?v_194) ?v_26)) (or (or ?v_226 ?v_255) ?v_88)) (or (or ?v_28 ?v_54) ?v_115)) (or (or ?v_148 ?v_115) ?v_90)) (or (or ?v_198 P47) ?v_32)) (or (or P41 ?v_191) P36)) (or (or P5 P40) P7)) (or (or ?v_157 ?v_266) ?v_21)) (or (or ?v_210 ?v_90) ?v_111)) (or (or ?v_47 ?v_158) ?v_94)) (or (or ?v_162 ?v_161) ?v_186)) (or (or P16 ?v_243) ?v_256)) (or (or ?v_155 ?v_13) ?v_104)) (or (or P3 ?v_168) ?v_111)) (or (or ?v_112 ?v_187) ?v_191)) (or (or ?v_252 P29) ?v_50)) (or (or P39 P11) ?v_10)) (or (or ?v_131 P31) P13)) (or (or ?v_32 ?v_161) ?v_214)) (or (or ?v_31 ?v_173) ?v_203)) (or (or P3 ?v_128) ?v_34)) (or (or ?v_219 ?v_124) ?v_148)) (or (or ?v_197 ?v_154) ?v_122)) (or (or ?v_232 ?v_144) ?v_85)) (or (or ?v_239 ?v_172) ?v_40)) (or (or ?v_191 ?v_145) ?v_115)) (or (or ?v_21 ?v_237) ?v_60)) (or (or ?v_208 ?v_75) P49)) (or (or ?v_26 ?v_191) ?v_23)) (or (or ?v_154 ?v_33) ?v_257)) (or (or P11 ?v_235) ?v_52)) (or (or ?v_225 ?v_187) ?v_197)) (or (or ?v_45 ?v_68) ?v_188)) (or (or ?v_221 ?v_222) P20)) (or (or ?v_33 ?v_205) ?v_23)) (or (or ?v_85 ?v_141) ?v_162)) (or (or ?v_64 P13) ?v_181)) (or (or ?v_103 P45) ?v_125)) (or (or P32 P8) ?v_238)) (or (or ?v_126 ?v_164) ?v_9)) (or (or ?v_24 ?v_62) ?v_133)) (or (or ?v_94 ?v_213) ?v_179)) (or (or ?v_6 ?v_12) ?v_186)) (or (or ?v_48 ?v_29) ?v_206)) (or (or ?v_158 ?v_50) ?v_205)) (or (or ?v_49 ?v_184) ?v_40)) (or (or P35 ?v_224) ?v_110)) (or (or ?v_134 P40) ?v_156)) (or (or ?v_247 ?v_96) ?v_105)) (or (or ?v_62 ?v_207) ?v_216)) (or (or ?v_157 ?v_151) ?v_206)) (or (or ?v_7 ?v_35) P27)) (or (or ?v_67 ?v_102) ?v_214)) (or (or ?v_76 P17) ?v_258)) (or (or P40 ?v_12) P43)) (or (or ?v_204 ?v_92) ?v_116)) (or (or ?v_248 ?v_142) ?v_189)) (or (or ?v_86 ?v_111) ?v_14)) (or (or P0 ?v_259) ?v_144)) (or (or ?v_100 ?v_122) P13)) (or (or ?v_157 ?v_88) ?v_163)) (or (or ?v_67 ?v_214) P25)) (or (or ?v_83 ?v_238) ?v_42)) (or (or ?v_258 ?v_132) ?v_45)) (or (or ?v_98 ?v_79) ?v_103)) (or (or ?v_256 ?v_85) P46)) (or (or ?v_247 P29) ?v_126)) (or (or ?v_6 ?v_76) P10)) (or (or ?v_236 P27) ?v_232)) (or (or ?v_198 ?v_46) ?v_229)) (or (or ?v_98 ?v_58) P18)) (or (or ?v_151 ?v_233) ?v_135)) (or (or ?v_153 ?v_202) ?v_246)) (or (or P39 ?v_181) ?v_218)) (or (or ?v_253 ?v_233) P2)) (or (or ?v_21 ?v_255) ?v_199)) (or (or ?v_112 P8) ?v_135)) (or (or ?v_75 ?v_174) P32)) (or (or ?v_196 P35) P41)) (or (or ?v_64 ?v_70) ?v_111)) (or (or P4 ?v_188) ?v_85)) (or (or ?v_196 ?v_74) ?v_48)) (or (or ?v_185 ?v_103) ?v_260)) (or (or ?v_62 ?v_188) ?v_152)) (or (or ?v_261 ?v_22) ?v_148)) (or (or P32 ?v_253) ?v_238)) (or (or ?v_217 P19) ?v_102)) (or (or P11 P38) ?v_207)) (or (or ?v_113 ?v_251) ?v_7)) (or (or ?v_148 ?v_207) ?v_124)) (or (or P5 ?v_117) ?v_211)) (or (or ?v_251 ?v_208) ?v_80)) (or (or ?v_239 ?v_153) ?v_4)) (or (or P7 ?v_215) ?v_190)) (or (or ?v_28 ?v_113) ?v_16)) (or (or ?v_157 ?v_147) ?v_152)) (or (or ?v_162 ?v_131) ?v_152)) (or (or ?v_262 ?v_263) ?v_111)) (or (or ?v_52 P48) ?v_98)) (or (or ?v_126 ?v_30) P16)) (or (or ?v_143 ?v_24) ?v_244)) (or (or ?v_64 P3) ?v_205)) (or (or ?v_151 ?v_163) P27)) (or (or ?v_155 ?v_211) ?v_6)) (or (or P3 ?v_264) ?v_162)) (or (or ?v_18 ?v_17) ?v_124)) (or (or ?v_49 ?v_81) ?v_189)) (or (or ?v_224 P27) ?v_187)) (or (or ?v_189 ?v_87) ?v_84)) (or (or ?v_160 ?v_150) ?v_102)) (or (or ?v_94 ?v_224) P32)) (or (or ?v_177 ?v_44) ?v_205)) (or (or ?v_239 ?v_165) ?v_207)) (or (or ?v_227 P15) ?v_94)) (or (or ?v_46 ?v_234) ?v_6)) (or (or ?v_15 P40) ?v_64)) (or (or ?v_264 ?v_38) ?v_64)) (or (or ?v_208 P12) ?v_52)) (or (or P47 ?v_200) ?v_262)) (or (or ?v_37 ?v_161) ?v_2)) (or (or ?v_58 ?v_55) ?v_199)) (or (or ?v_53 ?v_211) ?v_143)) (or (or ?v_223 ?v_199) ?v_16)) (or (or ?v_144 P7) ?v_111)) (or (or ?v_77 ?v_135) ?v_129)) (or (or ?v_135 ?v_153) ?v_131)) (or (or ?v_45 ?v_239) ?v_257)) (or (or ?v_176 ?v_41) ?v_259)) (or (or ?v_9 ?v_152) ?v_233)) (or (or P7 ?v_181) ?v_89)) (or (or P35 ?v_8) ?v_140)) (or (or ?v_140 ?v_265) ?v_25)) (or (or ?v_43 ?v_10) ?v_121)) (or (or ?v_135 ?v_247) ?v_67)) (or (or P23 ?v_216) ?v_226)) (or (or P15 ?v_263) ?v_45)) (or (or ?v_172 P16) ?v_103)) (or (or ?v_101 ?v_188) ?v_130)) (or (or ?v_198 P49) P22)) (or (or P36 ?v_24) ?v_227)) (or (or ?v_210 ?v_142) ?v_159)) (or (or ?v_23 ?v_32) ?v_61)) (or (or ?v_183 P24) ?v_255)) (or (or ?v_28 ?v_156) ?v_119)) (or (or ?v_180 ?v_44) ?v_154)) (or (or ?v_86 ?v_9) ?v_122)) (or (or ?v_176 ?v_33) P1)) (or (or ?v_263 P7) P25)) (or (or ?v_150 ?v_133) P38)) (or (or ?v_212 ?v_35) ?v_260)) (or (or ?v_122 ?v_256) ?v_217)) (or (or ?v_229 ?v_91) ?v_164)) (or (or ?v_191 ?v_188) ?v_179)) (or (or ?v_166 ?v_121) ?v_98)) (or (or ?v_32 ?v_257) ?v_58)) (or (or ?v_87 ?v_132) ?v_236)) (or (or ?v_259 ?v_238) ?v_174)) (or (or ?v_57 ?v_112) ?v_116)) (or (or P24 ?v_124) ?v_79)) (or (or ?v_41 ?v_111) ?v_242)) (or (or ?v_177 ?v_127) ?v_19)) (or (or ?v_203 P40) ?v_9)) (or (or ?v_213 ?v_207) ?v_244)) (or (or ?v_196 ?v_200) ?v_266)) (or (or ?v_25 ?v_246) P45)) (or (or ?v_256 ?v_15) ?v_91)) (or (or ?v_8 ?v_130) ?v_82)) (or (or ?v_54 ?v_2) ?v_207)) (or (or ?v_170 ?v_8) ?v_163)) (or (or ?v_215 ?v_50) ?v_60)) (or (or ?v_177 P41) ?v_44)) (or (or ?v_90 ?v_120) ?v_126)) (or (or ?v_165 ?v_165) ?v_195)) (or (or ?v_67 ?v_183) P37)) (or (or P46 ?v_101) ?v_216)) (or (or ?v_203 P7) ?v_197)) (or (or ?v_144 P20) ?v_16)) (or (or ?v_24 ?v_251) ?v_122)) (or (or ?v_258 ?v_12) ?v_171)) (or (or ?v_50 ?v_79) ?v_9)) (or (or ?v_192 ?v_191) ?v_169)) (or (or ?v_216 ?v_103) ?v_97)) (or (or ?v_235 ?v_265) ?v_47)) (or (or P7 P31) ?v_234)) (or (or ?v_255 ?v_220) ?v_196)) (or (or ?v_265 P47) ?v_156)) (or (or ?v_61 ?v_189) ?v_158)) (or (or ?v_93 ?v_17) ?v_75)) (or (or ?v_253 P23) ?v_247)) (or (or ?v_14 ?v_229) ?v_250)) (or (or P8 ?v_156) P16)) (or (or ?v_190 ?v_117) ?v_97)) (or (or ?v_241 ?v_259) P4)) (or (or ?v_257 ?v_104) ?v_175)) (or (or ?v_125 ?v_126) ?v_215)) (or (or ?v_238 ?v_116) ?v_176)) (or (or ?v_236 ?v_94) ?v_26)) (or (or P16 ?v_24) ?v_165)) (or (or ?v_213 ?v_190) P28)) (or (or P14 P40) ?v_9))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
